Add a mathematical constraint system#8816
Conversation
tlively
left a comment
tlively
left a comment
There was a problem hiding this comment.
I highly recommend explicitly framing the constraint space as a lattice:
- Both
and_andfuzzyOrare effectively merging constraints. You want both (but especiallyfuzzyOr) to have all the properties of a lattice join operator: monotonicity, associativity, commutativity, idempotency, etc. You also wantfuzzyOrto be as precise as possible; it has to lose some precision sometimes, but you only want it to lose as much precision as necessary given the representation of constraints. So you want it to be a least upper bound, i.e. a join. - Making the constraint space a lattice will give you all the nice properties you want for using it in a program analysis: order-independence, guaranteed convergence, etc. It also reduces all the novelty and complexity to just generating the constraints in the first place; getting to the fixed point after that is just the classic worklist + graph traversal pattern.
- Making the constraint space a lattice will let you test it in the lattice fuzzer, which can do a better job than just unit tests alone of making sure it has all the properties we want, including that we do not unnecessarily lose precision in the merge operation.
|
|
||
| // We limit constraints to a low number to ensure good performance even with | ||
| // simple brute-force solving. | ||
| // TODO: use a generic constraint solver..? |
There was a problem hiding this comment.
I did have that POC for pulling in Z3. In the limit I guess that's what we'd want. 5c2bbb7
| // { this } => { condition } | ||
| // | ||
| // https://en.wikipedia.org/wiki/Material_conditional#Truth_table | ||
| Result check(const Constraint& condition) const; |
There was a problem hiding this comment.
Hmm, yeah. Another option is eval as @MaxGraey suggests?
|
That's awesome! Have you considered more academic and conventional naming for lattice-like stuff?
or something like this? |
|
@tlively Definitely making this a lattice would have benefits, but it would add overhead and complexity, I worry. Specifically, having a limited capacity (number of constraints in a set), as in the current design, is really nice for efficiency, but makes it not a lattice. Here is a concrete example. For a lattice we need this absorption law:
which breaks the absorption rule. (This is sort of parallel to the issue with multiple constants in possible-constants - we only support one constant, not an arbitrary number. An arbitrary number is necessary for all the nice mathematical properties we want, but the overhead isn't worth it in GUFA.) |
Good idea, I think that makes sense.
I think this is clear enough already, and shorter?
I left this intentionally vague as this may expand in the future. A set of constraints is, atm, a conjunction, but if we find a nice way to allow OR and not just AND, we should add it. The idea is, conceptually, a set of constraints that can prove things. |
|
Btw binaryen already has some basic semi and full lattices: https://github.com/WebAssembly/binaryen/blob/main/src/analysis/lattice.h and https://github.com/WebAssembly/binaryen/blob/main/src/analysis/lattices/abstraction.h infra. So how about this? class LowerBound : Lattice { ... }
class UpperBound : FullLattice { ... }
class RangeBound : FullLattice { ... } |
Certainly you cannot have all three of these properties:
We both agree that we must give up on (3). I'm just saying that we should design the system such that we can still have (1) and (2) instead of just (2). Designing the system to be a lattice will require some care and perhaps some additional compromises on precision, but I strongly believe the benefits would be worth it. One option would be to come up with all the constraints we're interested in, then figure out how to structure them properly to make sure they form a lattice. Another way to keep things simple would be to use the product of multiple simpler lattices for the analysis. For example, we could simultaneously do a range analysis, sign analysis, and bit analysis, each of which is very simple to understand. Each individual component of the larger lattice could be developed independently. Otherwise we should just pull in Z3 rather than reinventing the wheel for an arbitrary constraint solver. |
3 participants
This allows defining constraints like
{ x >= 0 && x <= 100 }and to then check if theyimply something else is true or false, like
{ x >= 0 && x <= 100 } => { x < 9999 }(example of a valid inference).
This is the minimal first part of such a system, focusing on
==, !=, and very simplesolving. Putting up for design feedback before I work in depth on the rest.
Next steps are to add
>=, <etc., and to add a pass that uses this in a control-flowaware way, that is, the goal is to optimize things like
This is important to remove userspace bounds checks for Kotlin (and likely Java).
inplace_vectorpart here is from #8814 (will rebase once it lands).